T:Type, a:(T List), x:T. l_disjoint(T;a;[x])  ((x  a)) 

latex

Definitions	t  T, x:A. B(x), (x  l), A, P & Q, P  Q, False, , P  Q, P  Q, x. t(x), l_disjoint(T;l1;l2)
Lemmas	iff functionality wrt iff, all functionality wrt iff, not functionality wrt iff, and functionality wrt iff, member singleton, iff wf, not wf, l member wf